Nuprl Definition : ma-send
0,22
postcript
pdf
M
.send(
k
;
l
;
s
;
v
;
ms
;
i
)
==
L
!= 1of(2of(2of(2of(2of(2of(
M
))))))(<
k
,
l
>)
==
==
ms
= if source(
l
) =
i
concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;2of(
tgf
)(
s
,
v
));
L
)) else nil fi
latex
clarification:
M
.send(
k
;
l
;
s
;
v
;
ms
;
i
)
== fpf-val(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== fpf-val(
1of(2of(2of(2of(2of(2of(
M
))))));
== fpf-val(
<
k
,
l
>;
== fpf-val(
k
,
L
.(
ms
== fpf-val(
k
,
L
.(
=
== fpf-val(
k
,
L
.(
if source(
l
) =
i
concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;2of(
tgf
)(
s
,
v
));
L
)) else nil fi
== fpf-val(
k
,
L
.(
(
tg
:Id
if source(
l
) =
i
M
.da(rcv(
l
,
tg
)) else Top fi) List))
latex
Definitions
z
!=
f
(
x
)
P
(
a
;
z
)
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
IdLnk
,
KindDeq
,
IdLnkDeq
,
s
=
t
,
type
List
,
x
:
A
B
(
x
)
,
Id
,
M
.da(
a
)
,
rcv(
l
,
tg
)
,
Top
,
if
b
t
else
f
fi
,
a
=
b
,
source(
l
)
,
concat(
ll
)
,
map(
f
;
as
)
,
x
.
A
(
x
)
,
<
a
,
b
>
,
1of(
t
)
,
f
(
a
)
,
2of(
t
)
,
nil
FDL editor aliases
ma-send
origin